package com.solver.demo.smt;

import lombok.extern.slf4j.Slf4j;
import org.sosy_lab.common.ShutdownNotifier;
import org.sosy_lab.common.configuration.*;
import org.sosy_lab.common.configuration.converters.ClassTypeConverter;
import org.sosy_lab.common.configuration.converters.IntegerTypeConverter;
import org.sosy_lab.common.configuration.converters.TimeSpanTypeConverter;
import org.sosy_lab.common.log.BasicLogManager;
import org.sosy_lab.common.log.LogManager;
import org.sosy_lab.java_smt.SolverContextFactory;
import org.sosy_lab.java_smt.api.SolverContext;

@Slf4j
public class SmtSolverUtil {
    public static SolverContext solverContext() {
        try {
            Configuration config = configuration();
            LogManager logger = BasicLogManager.create(config);
            ShutdownNotifier notifier = ShutdownNotifier.createDummy();
            SolverContextFactory.Solvers solvers = SolverContextFactory.Solvers.Z3;
            SolverContext context = SolverContextFactory.createSolverContext(config, logger, notifier, solvers, SmtLibLoadUtil::loadLibrary);
            return context;
        } catch (InvalidConfigurationException e) {
            log.error("获取 SMT 引擎上下文失败", e);
        }
        return null;
    }

    private static Configuration configuration() {
        ConfigurationBuilder newConfig = Configuration.builder()
                .addConverter(Class.class, new ClassTypeConverter())
                .addConverter(ClassOption.class, new ClassTypeConverter())
                .addConverter(IntegerOption.class, new IntegerTypeConverter())
                .addConverter(TimeSpanOption.class, new TimeSpanTypeConverter())
                .setOption("timeout", "500");
        try {
            return newConfig.build();
        } catch (InvalidConfigurationException e) {
            log.error("获取 SMT 参数失败", e);
        }
        return null;
    }
}
